COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(proof lisp)
C00003 ENDMK
C⊗;
(proof lisp)

(DECL (U V W) |GROUND| VARIABLE LIST)

(DECL (X Y Z) |GROUND| VARIABLE SEXP)

(decl (a b c) |ground| variable)

(decl (assign) |ground⊗ground⊗ground→ground| constant)

(decl (contents) |ground⊗ground→ground| constant)

(axiom |∀ var val vec.contents(var,assign(var,val,vec)) = val|)

(axiom |∀ var val val1 vec.assign(var,val,assign(var,val,vec))
					 = assign(var,val,vec)|)

(axiom |∀ var1 var2 val1 val2 vec. ¬(var1 = var2) ⊃
	assign(var1,val1,assign(var2,val2,vec)) = 
		assign(var2,val2,assign(var1,val1,vec))|)

(axiom |∀e vec.eval(e,vec) =